We present a sequent calculus for the modal logic S4, and building on some relevant features of this system we show how S4 can easily be translated into full propositional linear logic, extending the Grishin-Ono translation of classical logic into linear logic. The translation introduces linear modalities only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.

We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\mathsf{S4}\) spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for \(\Box\) and \(\Diamond\). Starting points for this research are 2-sequents and indexed-based calculi (...) (sequents and tableaux). By extending and modifying existing proposals, we show how to achieve a syntactical proof of the cut-elimination theorem that is as close as possible to the one for first-order classical logic. In doing this, we implicitly show how small is the proof-theoretical distance between classical logic and the systems under consideration. (shrink)

The paper defends the position that phenomenological interviews can provide a rich source of knowledge and that they are in no principled way less reliable or less valid than quantitative or experimental methods in general. It responds to several skeptic objections such as those raised against introspection, those targeting the unreliability of episodic memory, and those claiming that interviews cannot address the psychological, cognitive and biological correlates of experience. It argues that the skeptic must either heed the methodological and epistemological (...) justification of the phenomenological interview provided, or embrace a more fundamental skepticism, a “deep mistrust”, in which scientific discourse can have no recourse to conscious processes as explananda, with ensuing dire consequences for our conception of science. (shrink)

Research in phenomenology has benefitted from using exceptional cases from pathology and expertise. But exactly how are we to generate and apply knowledge from such cases to the phenomenological domain? As researchers of cerebral palsy and musical absorption, we together answer the how question by pointing to the resource of the qualitative interview. Using the qualitative interview is a direct response to Varela’s call for better pragmatics in the methodology of phenomenology and cognitive science and Gallagher’s suggestion for phenomenology to (...) develop its methodology and outsource its tasks. We agree with their proposals, but want to develop them further by discussing and proposing a general framework that can integrate research paradigms of the well-established disciplines of phenomenological philosophy and qualitative science. We give this the working title, a “phenomenological interview”. First we describe the what of the interview, that is the nature of the interview in which one encounters another subject and generates knowledge of a given experience together with this other subject. In the second part, we qualify why it is worthwhile making the time-consuming effort to engage in a phenomenological interview. In the third and fourth parts, we in general terms discuss how to conduct the interview and the subsequent phenomenological analysis, by discussing the pragmatics of Vermersch’s and Petitmengin’s “Explicitation Interview”. (shrink)

While most large companies around the world now have a code of ethics, reported ethical malpractice among some of these does not appear to be abating. The reasons for this are explored, using academic studies, survey reports as well as insights gained from the Institute of Business Ethics' work with large corporations. These indicate that there is a gap between the existence of explicit ethical values and principles, often expressed in the form of a code, and the attitudes and behaviour (...) of the organisation. The paper suggests that two basic reasons appear to be at the heart of the problem: ineffective ethics programmes and deficiencies in corporate culture. The paper concludes that successfully embedded corporate ethical values requires well‐designed ethics policies, sustained ethical leadership and incorporation of ethics in organisational processes and strategy as part of an ethical culture at all levels of the organisation. It makes some practical suggestions on how this can be achieved. (shrink)

Raccolta di saggi sulla storia della filosofia rinascimentale e moderna.

In this paper, we advance the thesis that music-making can be advantageously understood as an exploratory phenomenon. While music-making is certainly about aesthetic expression, from a phenomenological, cognitive, and even evolutionary perspective, it more importantly concerns structured explorations of the world around us, our minds, and our bodies. Our thesis is based on an enactive and phenomenological analysis of three cases: the first concerns the study of infants involved in early musical activities, and the two latter are phenomenologically inspired interviews (...) with an expert jazz improviser, and members of a prominent string quartet. Across these examples, we find that music-making involves a dual intentionality - one oriented towards the exploration of the sonic, material, and social environment, and one oriented toward the self, including the exploration of bodily awareness and reflective mental states. In enactivist terms, exploration is a fundamental way of making sense of oneself as coupled with the world. Understanding music-making as a pre-eminent case of exploration helps us explicate and appreciate the developmental, sensorimotor, and more advanced cognitive resources that exist in music-making activities. (shrink)

While most large companies around the world now have a code of ethics, reported ethical malpractice among some of these does not appear to be abating. The reasons for this are explored, using academic studies, survey reports as well as insights gained from the Institute of Business Ethics' work with large corporations. These indicate that there is a gap between the existence of explicit ethical values and principles, often expressed in the form of a code, and the attitudes and behaviour (...) of the organisation. The paper suggests that two basic reasons appear to be at the heart of the problem: ineffective ethics programmes and deficiencies in corporate culture. The paper concludes that successfully embedded corporate ethical values requires well-designed ethics policies, sustained ethical leadership and incorporation of ethics in organisational processes and strategy as part of an ethical culture at all levels of the organisation. It makes some practical suggestions on how this can be achieved. (shrink)

Raccolta di saggi sulla storia della filosofia rinascimentale e moderna.

We provide a phenomenological explanation of the particular function mental images play in the realization of enjoyment and their significance for human freedom on the basis of the idea, drawn from Sartre, that images are not things but rather a way consciousness behaves towards objects. The mental image’s matter, which consists of affectivity, knowledge, and kinaesthetic operations, allows imagination to conjure up an unreal item to satiate a desire. However, by foreshadowing enjoyment in the imaginary, the mental image urges consciousness (...) toward a change in the world that would make that enjoyment real. This is accomplished through the development of tools, which rely on the ability to overcome not just a given situation but also courses of goal-oriented behaviour that have already been prepared by the environment. Through this creation, consciousness exerts its freedom within reality, and marks the world as meaningful. (shrink)

In Being Realistic About Reasons,T.M. Scanlon develops a non-naturalistic realist account of normative reasons. A crucial part of that account is Scanlon’s contention that there is no deep epistemological problem for non-naturalistic realists, and that the method of reflective equilibrium suffices to explain the possibility of normative knowledge. In this critical notice we argue that this is not so: on a realist picture, normative knowledge presupposes a significant correlation between distinct entities, namely between normative beliefs and normative facts. This correlation (...) calls for an explanation. We show that Scanlon does not have the resources to offer such an explanation. (shrink)

Auditory verbal hallucinations (AVHs) are a highly complex and rich phenomena, and this has a number of important clinical, theoretical and methodological implications. However, until recently, this fact has not always been incorporated into the experimental designs and theoretical paradigms used by researchers within the cognitive sciences. In this paper, we will briefly outline two recent examples of phenomenologically informed approaches to the study of AVHs taken from a cognitive science perspective. In the first example, based on Larøi and Woodward (...) (Harv Rev Psychiatry 15:109–117, 2007 ), it is argued that reality monitoring studies examining the cognitive underpinnings of hallucinations have not reflected the phenomenological complexity of AVHs in their experimental designs and theoretical framework. The second example, based on Jones (Schizophr Bull, in press, 2010 ), involves a critical examination of the phenomenology of AVHs in the context of two other prominent cognitive models: inner speech and intrusions from memory. It will be shown that, for both examples, the integration of a phenomenological analysis provides important improvements both on a methodological, theoretical and clinical level. This will be followed by insights and critiques from philosophy and clinical psychiatry—both of which offer a phenomenological alternative to the empiricist–rationalist conceptualisation of AVHs inherent to the cognitive sciences approach. Finally, the paper will conclude with ideas as to how the cognitive sciences may integrate these latter perspectives into their methodological and theoretical programmes. (shrink)

Auditory verbal hallucinations (AVHs) are a highly complex and rich phenomena, and this has a number of important clinical, theoretical and methodological implications. However, until recently, this fact has not always been incorporated into the experimental designs and theoretical paradigms used by researchers within the cognitive sciences. In this paper, we will briefly outline two recent examples of phenomenologically informed approaches to the study of AVHs taken from a cognitive science perspective. In the first example, based on Larøi and Woodward (...) (Harv Rev Psychiatry 15:109–117, 2007), it is argued that reality monitoring studies examining the cognitive underpinnings of hallucinations have not reflected the phenomenological complexity of AVHs in their experimental designs and theoretical framework. The second example, based on Jones (Schizophr Bull, in press, 2010), involves a critical examination of the phenomenology of AVHs in the context of two other prominent cognitive models: inner speech and intrusions from memory. It will be shown that, for both examples, the integration of a phenomenological analysis provides important improvements both on a methodological, theoretical and clinical level. This will be followed by insights and critiques from philosophy and clinical psychiatry—both of which offer a phenomenological alternative to the empiricist–rationalist conceptualisation of AVHs inherent to the cognitive sciences approach. Finally, the paper will conclude with ideas as to how the cognitive sciences may integrate these latter perspectives into their methodological and theoretical programmes. (shrink)

Masini, A., 2-Sequent calculus: a proof theory of modalities, Annals of Pure and Applied Logic 58 229–246. In this work we propose an extension of the Getzen sequent calculus in order to deal with modalities. We extend the notion of a sequent obtaining what we call a 2-sequent. For the obtained calculus we prove a cut elimination theorem.

This article highlights major results of a study into the ethical norms and rules governing biobanks. After describing the methodology, the findings regarding four topics are presented: (1) the ownership of human biological samples held in biobanks; (2) the regulation of researchers’ use of samples obtained from biobanks; (3) what constitutes “collective consent” to genetic research, and when it is needed; and (4) benefit sharing and remuneration of research participants. The paper then summarizes key lessons to be drawn from the (...) findings and concludes by reflecting on the importance of such empirical research to inform future governance norms and practices. (shrink)

The beneficial effects of physical exercise on physical health and cognitive functioning have been repeatedly shown. However, evidence of its effect on psychosocial functioning in healthy adults is still scarce or inconclusive. One limitation of many studies examining this link is their reliance on correlational approaches or specific subpopulations, such as clinical populations. The present study investigated the effects of a physical exercise intervention on key factors of psychosocial functioning, specifically well-being, stress, loneliness, and future time perspective. We used data (...) from healthy, previously sedentary older adults who participated in a 6-month at-home intervention, either engaging in aerobic exercise or as part of a control group who participated in foreign language-learning or reading of selected native-language literature. Before and after the intervention, comprehensive cardiovascular pulmonary testing and a psychosocial questionnaire were administered. The exercise group showed significantly increased fitness compared to the control group. Contrary to expectations, however, we did not find evidence for a beneficial effect of this fitness improvement on any of the four domains of psychosocial functioning we assessed. This may be due to pronounced stability of such psychological traits in older age, especially in older adults who show high levels of well-being initially. Alternatively, it may be that the well-documented beneficial effects of physical exercise on brain structure and function, as well as cognition differ markedly from beneficial effects on psychosocial functioning. While aerobic exercise may be the driving factor for the former, positive effects on the latter may only be invoked by other aspects of exercise, for example, experiences of mastery or a feeling of community. (shrink)

We introduce a two‐dimensional metric (interval) temporal logic whose internal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then we prove completeness and a semantic partial cut elimination theorem down to formulas of a certain type.

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A∪B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and ẃ. This “ambivalent” nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in (...) contrast, we make explicit this duality of until by introducing a new temporal operator ∇ that allows us to formalize the “history” of until, i.e., the “internal” universal quantification over the time instants between the current one and ẃ. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system N(LTL∇) for a linear-time logic LTL∇ endowed with the new history operator. We show that LTL∇ is equivalent to the linear temporal logic LTL with until, which follows by formalizing back and forth translations between the two logics. We also define an indirect translation from LTL∇ into LTL via temporal logics with past operators; such a result provides an upper bound to the problem of satisfiability for LTL∇ formulas. (shrink)

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A∪B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and ẃ. This “ambivalent” nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in (...) contrast, we make explicit this duality of until by introducing a new temporal operator ∇ that allows us to formalize the “history” of until, i.e., the “internal” universal quantification over the time instants between the current one and ẃ. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system N(LTL∇) for a linear-time logic LTL∇ endowed with the new history operator. We show that LTL∇ is equivalent to the linear temporal logic LTL with until, which follows by formalizing back and forth translations between the two logics. We also define an indirect translation from LTL∇ into LTL via temporal logics with past operators; such a result provides an upper bound to the problem of satisfiability for LTL∇ formulas. (shrink)

Despite a long history of researchers who combine phenomenology with qualitative or quantitative methods, there are only few examples of working with a phenomenological mixed method—a method where phenomenology informs both qualitative and quantitative data generation, analysis, and interpretation. Researchers have argued that in working with a phenomenological mixed method, there should be mutual constraint and enlightenment between the qualitative and quantitative methods for studying consciousness. In this article, we discuss what a framework for phenomenological mixed methods could look like (...) and we aim to provide guidance of how to work within such framework. We are inspired by resources coming from research in mixed methods and existing examples of phenomenological mixed-method research. We also present three cases of phenomenological mixed methods where we study complex social phenomena and discuss the process of how we conducted the studies. From both the research inspiration and our own studies, we depict the landscape of possibilities available for those interested in mixing phenomenology with qualitative and quantitative methods, as well as the challenges and common pitfalls that researchers face. To navigate in this landscape, we develop a three-fold structure, focusing on the phenomenological frame, the phenomenologically informed generation of qualitative and quantitative data, and the phenomenologically informed analysis and interpretation of data. (shrink)

We introduce an extension of natural deduction that is suitable for dealing with modal operators and induction. We provide a proof reduction system and we prove a strong normalization theorem for an intuitionistic calculus. As a consequence we obtain a purely syntactic proof of consistency. We also present a classical calculus and we relate provability in the two calculi by means of an adequate formula translation.

Precision medicine is an emerging approach to individualized care. It aims to help physicians better comprehend and predict the needs of their patients while effectively adopting in a timely manner the most suitable treatment by promoting the sharing of health data and the implementation of learning healthcare systems. Alongside its promises, PM also entails the risk of exacerbating healthcare inequalities, in particular between ethnoracial groups. One often-neglected underlying reason why this might happen is the impact of structural racism on PM (...) initiatives. Raising awareness as to how structural racism can influence PM initiatives is paramount to avoid that PM ends up reproducing the pre-existing health inequalities between different ethnoracial groups and contributing to the loss of trust in healthcare by minority groups. We analyse three nodes of a process flow where structural racism can affect PM’s implementation. These are: the collection of biased health data during the initial encounter of minority groups with the healthcare system and researchers, the integration of biased health data for minority groups in PM initiatives and the influence of structural racism on the deliverables of PM initiatives for minority groups. We underscore that underappreciation of structural racism by stakeholders involved in the PM ecosystem can be at odds with the ambition of ensuring social and racial justice. Potential specific actions related to the analysed nodes are then formulated to help ensure that PM truly adheres to the goal of leaving no one behind, as endorsed by member states of the United Nations for the 2030 Agenda for Sustainable Development. Structural racism has been entrenched in our societies for centuries and it would be naïve to believe that its impacts will not spill over in the era of PM. PM initiatives need to pay special attention to the discriminatory and harmful impacts that structural racism could have on minority groups involved in their respective projects. It is only by acknowledging and discussing the existence of implicit racial biases and trust issues in healthcare and research domains that proper interventions to remedy them can be implemented. (shrink)

Loss aversion can occur in riskless and risky choices. We present novel evidence on both in a non-student sample (660 randomly selected customers of a car manufacturer). We measure loss aversion in riskless choice in endowment effect experiments within and between subjects and find similar levels of average loss aversion in both. The subjects of the within study also participate in a simple lottery choice task which arguably measures loss aversion in risky choices. We find substantial heterogeneity in both measures (...) of loss aversion. Loss aversion in riskless choice and loss aversion in risky choice are strongly positively correlated, but on average riskless loss aversion is higher than risky loss aversion. We find that in both choice tasks, loss aversion increases in age, income, and wealth, and decreases in education. Our results provide novel supportive input to the debate about the reality of loss aversion. (shrink)

The contact hypothesis has dominated work on prejudice reduction and is often described as one of the most successful theories within social psychology. The hypothesis has nevertheless been criticized for not being applicable in real life situations due to unobtainable conditions for direct contact. Several indirect contact suggestions have been developed to solve this “application challenge.” Here, we suggest a hybrid strategy of both direct and indirect contact. Based on the second-person method developed in social psychology and cognition, we suggest (...) working with an engagement strategy as a hybrid hypothesis. We expand on this suggestion through an engagement-based intervention, where we implement the strategy in a theater performance and investigate the effects on prejudicial attitudes toward people with physical disabilities. Based on the results we reformulate our initial engagement strategy into the Enact hypothesis. To deal with the application challenge, this hybrid hypothesis posits two necessary conditions for prejudice reduction. Interventions should: work with engagement to reduce prejudice, and focus on the second-order level of attitudes formation. Here the aim of the prejudice reduction is not attitude correction, but instead the nuancing of attitudes. (shrink)

O estudo investigou indicadores da síndrome de couvade em pais primíparos durante a gravidez das esposas. Participaram 30 casais com idades entre 20 e 35 anos que estavam em diferentes trimestres da gestação. Os pais e as gestantes responderam individualmente a uma entrevista semi-estruturada que in..

Cancer registries are an important part of the public health infrastructure, since they allow to monitor the temporal trends of this illness as well as facilitate epidemiological research. In order to effectively set up such registries, it is necessary to create a system of data collection that permits to record health-related information from patients who are diagnosed with cancer. Given the sensitive nature of such data, it is debated whether their recording should be based on consent or whether alternative arrangements (...) are possible (eg, opt-out systems where information is automatically collected but patients can later withdraw). In the recent reform of the Swiss cancer registration legislation, the lawmaker set out to implement rules about the recording of data in cancer registries that would allegedly go beyond a consent-based model, in order to balance accurate registration with respect of patient rights. However, by analysing the operational norms of the new legislation and comparing them with those of other systems, it emerges that the Swiss rules de facto closely resemble a system of registration based on informed consent—in partial contradiction with the objective pursued by the lawmaker. In this paper, we show how the details of a policy are crucial to determine its true nature and we highlight some critical elements—from an ethical standpoint—of the recently reformed Swiss policy on cancer registration. (shrink)

The meaning of a formula built out of proof-functional connectives depends in an essential way upon the intensional aspect of the proofs of the component subformulas. We study three such connectives, strong equivalence (where the two directions of the equivalence are established by mutually inverse maps), strong conjunction (where the two components of the conjunction are established by the same proof) and relevant implication (where the implication is established by an identity map). For each of these connectives we give a (...) type assignment system, a realizability semantics, and a completeness theorem. This form of completeness implies the semantic completeness of the type assignment system. (shrink)

Although developmental dyslexia (DD) is frequently associate to a phonological deficit, the underlying neurobiological cause remain undetermined. One prominent hypothesis suggests a specific deficit in magnocellular-dorsal (M-D) pathway. Here we investigated the visual M-D and parvocellular-ventral (P-V) pathway in dyslexic and in chronological age and IQ-matched normally reading children by measuring dynamic (frequency doubling illusion) and static stimuli sensibility, respectively. A specific deficit in M-D task was found. Importantly, the M-D deficit was selectively shown in poor phonological decoders. M-D deficit (...) appears to be frequent because 75% of poor pseudo-word readers were at least 1 SD below the mean of the controls. Finally, a replication study by using a new group of poor phonological decoders and reading level controls suggests a possible role of M-D deficit in DD. These results showed that a M-D deficit might impair the sub-lexical mechanisms that are critical for reading development. The possible link between these findings and the oscillatory “temporal sampling” framework is discussed. (shrink)

The interdisciplinary Hannover Qualification Programme on ethics consultation has trained hospital staff to operate clinical ethics services in their respective hospitals since 2003. To evaluate Hannover Qualification Programme, all former participants were contacted using an online questionnaire including four domains: status quo before attending Hannover Qualification Programme, present status, impact of Hannover Qualification Programme, future challenges. Research objectives were the long-term satisfaction with Hannover Qualification Programme and its impact on clinical ethics services. The response rate was 45%. Hannover Qualification Programme (...) was evaluated as helpful and the responders were capable of applying their acquired skills. Most participants could contribute to the implementation of clinical ethics services. They were satisfied with Hannover Qualification Programme and with the degree of changes in their hospitals. In conclusion, clinical ethics education had long-term effects on trainees and on their respective hospitals. Problems were mentioned rather in the field of utilisation than with implementation or quality of clinical ethics services. (shrink)

The Hannover qualifying programme ‘ethics consultation in hospitals’, conducted by a four-institution cooperation partnership, is an interdisciplinary, scientifically based programme for healthcare professionals interested in ethics consultation services and is widely acknowledged by hospital managements and healthcare professionals. It is unique concerning its content, scope and teaching format. With its basic and advanced modules it has provided training and education for 367 healthcare professionals with 570 participations since 2003 (until February 2010). One characteristic feature is its attractiveness for health professionals (...) from different backgrounds. Internationally, the Hannover programme is one of the few schedules with both academics and non-academics as target groups and a high participation rate of physicians. The concept of the Hannover programme is in great demand, and its schedule is continuously optimised through evaluation. The goals of enabling healthcare professionals from different professional backgrounds to define and reflect ethical problems, to facilitate and support the process of decision-making and to work out structures for their own institutions seem to have been achieved. However, in order to obtain effective and sustainable results, participation in the programme should be supplemented regularly by in-house training sessions or individual expert consultations. Future challenges include new thematic courses and providing a network for former participants, especially when they come from non-academic hospitals. The network is a reasonable platform to discuss participants' experiences, successes and pitfalls. A further task will be research on how the programme's concept can support the sustainability of ethics structures in the various institutions. (shrink)

Deep Brain Stimulation (DBS) is an effective treatment for advanced Parkinson’s disease. However, identifying stimulation parameters, such as contact and current amplitudes, is time-consuming based on trial and error. Directional leads add more stimulation options and render this process more challenging with a higher workload for neurologists and more discomfort for patients. In this study, a sweet spot-guided algorithm was developed that automatically suggested stimulation parameters. These suggestions were retrospectively compared to clinical monopolar reviews. A cohort of 24 Parkinson’s disease (...) patients underwent bilateral DBS implantation in the subthalamic nucleus at our center. First, the DBS’ leads were reconstructed with the open-source toolbox Lead-DBS. Second, a sweet spot for rigidity reduction was set as the desired stimulation target for programming. This sweet spot and estimations of the volume of tissue activated were used to suggest (i) the best lead level, (ii) the best contact, and (iii) the effect thresholds for full therapeutic effect for each contact. To assess these sweet spot-guided suggestions, the clinical monopolar reviews were considered as ground truth. In addition, the sweet spot-guided suggestions for best lead level and best contact were compared against reconstruction-guided suggestions, which considered the lead location with respect to the subthalamic nucleus. Finally, a graphical user interface was developed as an add-on to Lead-DBS and is publicly available. With the interface, suggestions for all contacts of a lead can be generated in a few seconds. The accuracy for suggesting the best out of four lead levels was 56%. These sweet spot-guided suggestions were not significantly better than reconstruction-guided suggestions (p = 0.3). The accuracy for suggesting the best out of eight contacts was 41%. These sweet spot-guided suggestions were significantly better than reconstruction-guided suggestions (p < 0.001). The sweet spot-guided suggestions of each contact’s effect threshold had a mean error of 1.2 mA. On an individual lead level, the suggestions can vary more with mean errors ranging from 0.3 to 4.8 mA. Further analysis is warranted to improve the sweet spot-guided suggestions and to account for more symptoms and stimulation-induced side effects. (shrink)

Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an ω–type schema of inference that naturally interpret the propositional and the predicate until–free fragments of Linear Time Logic LTL respectively. The two calculi are based on a natural extension of ordinary sequents and of standard modal rules. We examine the pure propositional case (no extralogical axioms), the propositional and the first order predicate cases (both with a possibly infinite set of (...) extralogical axioms). For each system we provide a syntactic proof of cut elimination and a proof of completeness. (shrink)

We investigate the consequences of removing the infinitary axiom and rules from a previously defined proof system for a fragment of propositional metric temporal logic over dense time.